{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs,
  ScopedTypeVariables, MultiParamTypeClasses, FlexibleContexts,
  FlexibleInstances, UndecidableInstances, TemplateHaskell #-}

{- |

Module      :  Data.Yoko.Algebra
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Catamorphism for mutually-recursive datatypes.

-}
module Data.Yoko.Cata
  (Algebras, SiblingAlgs, algebras, CataU(..), catas, cata, cataTo, sibCata, sibCataTo,
  module Data.Yoko.Reduce) where
    
import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect
import Data.Yoko.Reduce





type Algebras u m = NT u (Algebra m)
type SiblingAlgs t m = Algebras (DTs t) m

-- | Builds an 'NT' of algebras via 'AlgebraDT'.
algebras :: forall u m. (u :=> AlgebraU m) => [qP|m|] -> Algebras u m
algebras _ = NT $ (\AlgebraU -> algebraDT) . weakenTo [qP|AlgebraU m :: *->*|]



-- | @t@ is member of @CataU m@ if
--
--   1. @t@ is an instance of 'DT'
--
--   2. the recursive reduction can be mapped as a 'FromAt' function via
--   'RMMap' across all constructors of @t@ and
--
--   3. all of @t@'s siblings also inhabit the same type set.
data CataU u m t where
  CataU :: (DT t,
            DCs t :=>
              (YieldsArrowTSSU
               (AsComp (RMMap u (FromAt m) IdM :. N))),
            u :=> CataU u m,
            t ::: u
           ) => CataU u m t
obvious_membership ''CataU

catas :: forall u m. (u :=> CataU u m) => Algebras u m -> NT u (FromAt m IdM)
catas fs = firstNT (weakenTo [qP|CataU u m :: *->*|]) $
           NT $ \d@CataU -> cataD d fs

cataD :: DT t => CataU u m t -> Algebras u m -> t -> Med m t
cataD CataU fs =
  appNT fs membership .
  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
             RMMap $ catas fs) . disband

-- | Uses the @m@-mediated algebras for @u@ to reduce a @t@ to @Med m t@.
cata :: (DT t, t ::: CataU u m) => Algebras u m -> t -> Med m t
cata = cataD membership

-- | Specify the mediator directly, since it might not be determined by the
-- first argument.
cataTo :: (DT t, t ::: CataU u m) => [qP|m|] -> Algebras u m -> t -> Med m t
cataTo _ = cata

-- | Fixes @cata@'s @u@ as @DTs t@.
sibCata :: (DT t, t ::: CataU (DTs t) m) => SiblingAlgs t m -> t -> Med m t
sibCata = cata

-- | Specify the mediator directly and fix the type set to be @t@'s siblings.
sibCataTo :: (DT t, t ::: CataU (DTs t) m) => [qP|m|] -> SiblingAlgs t m -> t -> Med m t
sibCataTo _ = cata
